S. Valentini; 1983; "The Modal Logic of Provability: Cut-Elimination"
メモ
GLのシークエント計算
のカット除去定理について．
G. Gentzen; "Untersuchungen über das logische Schließen"
では
カット式
のdegree
と
証明図の高さ
による2重の帰納法なのに対し
こちらは更に
カット式のwidth
を足した3重の帰納法になっている．
いくつかスケッチレベルの証明があるらしいので，詳しくは後の時代の
R. Goré, R. Ramanayake; 2008; "Valentini's Cut-Elimination for Provability Logic Resolved"
を読んだほうが良いかも知らない．